Nuprl Lemma : subtype-fpf-general
11,40
postcript
pdf
A
:Type{i},
P
:(
A
{i}),
B
:(
A
Type{j}).
a
:{
a
:
A
|
P
(
a
)} fp
B
(
a
)
r
a
:
A
fp
B
(
a
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
S
T
,
suptype(
S
;
T
)
,
Type
,
type
List
,
<
a
,
b
>
,
x
:
A
B
(
x
)
,
,
a
:
A
fp
B
(
a
)
,
x
(
s
)
,
f
(
a
)
,
{
x
:
A
|
B
(
x
)}
,
(
x
l
)
,
x
:
A
B
(
x
)
,
P
Q
,
l
[
i
]
,
||
as
||
,
A
B
,
,
False
,
P
&
Q
,
P
Q
,
{
T
}
,
P
Q
,
T
,
True
,
s
=
t
,
A
,
,
A
c
B
,
#$n
,
a
<
b
,
x
:
A
.
B
(
x
)
Lemmas
length
wf1
,
select
wf
,
cons
member
,
nil
member
,
l
member
wf
origin
A:Type{i}, P:(A
{i}), B:(AType{j}). a:{a:A| P(a)} fp B(a) 
r a:A fp B(a) A:Type{i}, P:(A{i}), B:(AType{j}). a:{a:A| P(a)} fp B(a) r a:A fp B(a) 
Tx:A. B(x) T
B(x) B(a) l)B(x)
Q
B
Q
Q
T
A
B
x:A. B(x)